package tableaux;

import kb.TBox;
import kb.SimpleReasoning;

import java.util.*;

//import domain.*;
import domain.tc.InitDomainGraph;
import entities.*;
import entities.concept.Concept;
import entities.concept.DomainConcept;
import entities.concept.NotConcept;
import entities.concept.PConcept;

/**
 * 
 * Given a node, or a set of nodes, decide if any clash exists in the nodes.
 * f<g, g<f ->clash k1<f, f<k2 -> decide if k1<k2? f=k1, f=k2, k1!=k2 ->clash
 * 
 * @author j55wu
 * 
 */
public class ClashTrigger {

	private TBox tb;
	private SimpleReasoning sr;
	private Set<Concept> clashCPs;

	public ClashTrigger(TBox tb) {
		this.tb = tb;
		sr = new SimpleReasoning(this.tb);
		clashCPs = new HashSet<Concept>();
	}

	public Set<Concept> getClashingConcepts() {
		return this.clashCPs;
	}

	public void clearClashes() {
		this.clashCPs.clear();
	}

	public void addClashCp(Concept cp) {
		this.clashCPs.add(cp);
	}

	public boolean clashFound(Individual ind) {
		boolean clash = false;
		if (ind.getLabels().size() < 1) {
			// System.out.println("No concepts found in this individual's label.");
			return clash;
		}
		// return clashInLabels(preprocessor.Simplification.NNF(n.getLabels()));
		return clashInLabels(ind.getLabels());
	}

	// true if there is a contradiction!
	public boolean clashInLabels(Set<Concept> cs) {
		boolean clashfound = false;
		// for a set, test if all A super classes and all ~B subclasses are
		// disjoint.
//		Set<Concept> positives = new HashSet<Concept>(cs.size());
		Set<Concept> negatives = new HashSet<Concept>(cs.size());
		Set<DomainConcept<?, ?>> ds = new HashSet<DomainConcept<?, ?>>();
		for (Concept c : cs) {
			// in case we have top/bot in our language
			if (c.isBot()) {
				this.clashCPs.add(c);
				return true;
			} else if (c instanceof NotConcept) {
				Concept cnc = ((NotConcept) c).getConcept();
				if (cnc.isTop()) {
					this.clashCPs.add(c);
					return true;
				}
				// get all subclasses of cnc, as A->B implies that ~B->~A
				// negatives.addAll(sr.givenSubclasses(cnc));
				negatives.add(cnc);
			} else if (c instanceof DomainConcept) {
				ds.add((DomainConcept<?, ?>) c);
			} 
//			else {
//				try {
//					// positives.addAll(sr.givenSuperclasses(c));
//					positives.add(c);
//				} catch (Exception ex) {
//					ex.printStackTrace();
//				}
//			}
		}
		// Test whether clashes exist.
//		clashfound |= !Collections.disjoint(positives, negatives);
		negatives.retainAll(cs);
		clashfound |= !negatives.isEmpty();
		if (clashfound) {
			// get the clashing concepts
//			this.disjointSets(positives, negatives);
//			negatives.retainAll(cs);
			for (Concept p : negatives) {
				this.clashCPs.add(p);
				this.clashCPs.add(new NotConcept(p));
			}
		}

		if (ds.size() >= 1) {
			clashfound |= this.clashConcreteConcepts(ds);
		}
		return clashfound;
	}
	
//	private void setClash(Concept pc){
//		this.clashCPs.add(pc);
//		this.clashCPs.add(new NotConcept(pc));
//		return;
//	}

//	private void disjointSets(Collection<Concept> pos, Collection<Concept> neg) {
////		for (Concept p : pos) {
////			if (neg.contains(p)) {
////				setClash(p);
////			}
////		}
//		neg.retainAll(pos);
//		for (Concept p : neg) {
//			setClash(p);
//		}
//		return;
//	}

	/**
	 * true if any clash
	 */
	public boolean clashConcreteConcepts(Set<DomainConcept<?, ?>> cs) {
		long st = System.currentTimeMillis();
		InitDomainGraph g = new InitDomainGraph(cs, this);
		boolean ret = g.clashFinder();
		/**
		 * Note that I currently used a conservative way to get clashing
		 * features i.e., all current domain concept building the graph are
		 * considered This may degrade performance: need an efficient algorithm
		 * inside this TC algorithm
		 */
		if (ret) {
			this.clashCPs.addAll(cs);
		}
		long end = System.currentTimeMillis() - st;
		InitDomainGraph.timeSpend += end;
		InitDomainGraph.called++;
		return ret;
	}

	// for all the f feature concepts
	public boolean clashOfEQ(HashSet<DomainConcept<?, ?>> dcs) {
		HashMap<Object, HashSet<Object>> fmap = this.computeTransitiveClosure(
				dcs, new HashMap<Object, HashSet<Object>>());
		for (Object f : fmap.keySet()) {
			// if f =k1 and f=k2 and k1!=k2, then clash
			if (fmap.get(f).size() < 2) {
				continue;
			}
			int count = 0;
			for (Object o : fmap.get(f)) {
				if (o instanceof String) {
					count++;
				}
				if (count > 1) {
					// two values for the same feature!
					return false;
				}
			}
		}
		return true;
	}

	public boolean clashOfLT(HashSet<DomainConcept<?, ?>> lt) {
		HashMap<Object, HashSet<Object>> fmap = this.computeTransitiveClosure(
				lt, new HashMap<Object, HashSet<Object>>());
		for (Object f : fmap.keySet()) {
			// if f<f, then unsat!
			if (fmap.get(f).contains(f)) {
				return false;
			}
		}
		return true;
	}

	/*
	 * Only consider ?<?, ?<=?
	 */
	public HashMap<Object, HashSet<Object>> computeTransitiveClosure(
			HashSet<DomainConcept<?, ?>> ds,
			HashMap<Object, HashSet<Object>> map) {
		boolean update = false;
		for (DomainConcept<?, ?> dc : ds) {
			/*
			 * if(!(dc instanceof DomainConceptLT) && !(dc instanceof
			 * DomainConceptLTEQ)){ //not considered continue; }
			 */
			Object f = dc.getLHS();
			Object g = dc.getValue();
			if (map.containsKey(f)) {
				if (!map.get(f).contains(g)) {
					map.get(f).add(g);
					if (map.containsKey(g)) {
						map.get(f).addAll(map.get(g));
					}
					update |= true;
				}
			} else {
				update |= true;
				map.put(f, new HashSet<Object>());
				map.get(f).add(g);
				if (map.containsKey(g)) {
					map.get(f).addAll(map.get(g));
				}
			}
		}
		// if any update to any entry, then update the whole map
		if (update) {
			map = this.saturation(map);
		}
		return map;
	}

	// a simple recursion to compute transitive closure.
	public HashMap<Object, HashSet<Object>> saturation(
			HashMap<Object, HashSet<Object>> map) {
		boolean update = false;
		for (Object f : map.keySet()) {
			HashSet<Object> ds = map.get(f);
			int size1 = ds.size();
			if (ds.size() < 1) {
				continue;
			}
			for (Object g : ds) {
				if (map.containsKey(g)) {
					map.get(f).addAll(map.get(g));
				}
			}
			// if set enlarged -> true
			update |= size1 < map.get(f).size();
		}
		if (update) {
			map = saturation(map);
		}
		return map;
	}

}
